:- use_module(library(clpr)).

/* succeeds if C ==> B */
abstract_state_implies(C, B) :- 
	
	C = abs_state(C_Untrusted, C_Rewritten, C_ConstraintList),
	B = abs_state(B_Untrusted, B_Rewritten, B_ConstraintList),

	C_Untrusted = state(C_Un_H, [C_UEE|C_Un_EEList], C_Un_Trace, automaton(CUA)),
	C_Rewritten = state(C_Re_H, [C_REE|C_Re_EEList], C_Re_Trace, automaton(CRA)),	

	C_UEE = env(ScopeStackUC,OperandStackUC,RegFileUC),
	C_REE = env(ScopeStackRC,OperandStackRC,RegFileRC),
	
	B_Untrusted = state(B_Un_H, [B_UEE|B_Un_EEList], B_Un_Trace, automaton(BUA)),	
	B_Rewritten = state(B_Re_H, [B_REE|B_Re_EEList], B_Re_Trace, automaton(BRA)),
	
	B_UEE = env(ScopeStackUB,OperandStackUB,RegFileUB),
	B_REE = env(ScopeStackRB,OperandStackRB,RegFileRB),

/*	writeln('\n'),
	writeln('clp check.............'),
	writeln('printing C:'),
	print_abstract_state(C),
	writeln('printing B:'),
	print_abstract_state(B),
	writeln('......................\n'),*/

	/* TWO STEP PROCESS FOR CONSISTENCY CHECK */

	/* Step 1: Unification */
	%unify_stack(ScopeStackUC, ScopeStackUB),
	%unify_stack(ScopeStackRC, ScopeStackRB),
	ScopeStackUC = ScopeStackUB,
	ScopeStackRC = ScopeStackRB,

	%unify_stack(OperandStackUC, OperandStackUB),
	%unify_stack(OperandStackRC, OperandStackRB),
	OperandStackUC = OperandStackUB,
	OperandStackRC = OperandStackRB,

	%unify_registers(RegFileUC, RegFileUB),
	%unify_registers(RegFileRC, RegFileRB),
	%RegFileUC = RegFileUB,
	%RegFileRC = RegFileRB,

	%unify_registers(C_Un_Trace, B_Un_Trace),
	%unify_registers(C_Re_Trace, B_Re_Trace),
	C_Un_Trace = B_Un_Trace,
	C_Re_Trace = B_Re_Trace,

	CUA = BUA,
	CRA = BRA,

	/* Step 2: Constraint Solving */				  
	check_constraints(C_ConstraintList,B_ConstraintList).

check_constraint_list(X) :-
	{CL = A}, {A =< 2}.


check_constraints(C_ConstraintList,B_ConstraintList) :-
	{0 = 0}.				  

unify_registers([], _).
unify_registers([A|T1], [A|T2]) :- unify_registers(T1, T2).

unify_stack([], []).
unify_stack([A|T1], [A|T2]) :- unify_stack(T1, T2).
unify_stack([H1|T1],[H2|T2]) :- 
	H1 \= H2,
	unify_stack([H1|T1], [T2]).


print_abstract_state(abs_state(UnstrustedState, RewrittenState, ConstraintList)) :-
	UnstrustedState = state(H1, [EE1|EEList1], Trace1, _A1),
	RewrittenState = state(H2, [EE2|EEList2], Trace2, _A2),

	EE1 = env(ScopeStack1,OperandStack1,RegFile1),
	EE2 = env(ScopeStack2,OperandStack2,RegFile2),

	format('UntrustedHeap = ~w, UntrustedTrace = ~w~n', [H1,Trace1]),
	format('UntrustedEE = ~w~n',[EE1]),
	format('UntrustedEEList = ~w~n~n',[EEList1]),

	format('ReHeap = ~w, ReTrace = ~w~n', [H2,Trace2]),
	format('RewrittenEE = ~w~n',[EE2]),
	format('RewrittenEEList = ~w~n~n',[EEList2]),

	format('ConstraintList = ~w~n~n', [ConstraintList]).
